Nuprl Lemma : mon_itop_unroll_base
13,42
postcript
pdf
g
:IMonoid,
i
,
j
:
. (
i
=
j
)
(
E
:({
i
..
j
}
|
g
|). (
i
k
<
j
.
E
(
k
)) = e
|
g
|)
latex
Up
groups
1
Definitions of Statement
lb
i
<
ub
.
E
(
i
)
Definitions
lb
i
<
ub
.
E
(
i
)
Lemmas
itop
unroll
base
origin